f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
↳ QTRS
↳ DependencyPairsProof
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
G(cons(x, k), d) → G(k, cons(x, d))
F(a, cons(x, k)) → F(cons(x, a), k)
F(a, empty) → G(a, empty)
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
G(cons(x, k), d) → G(k, cons(x, d))
F(a, cons(x, k)) → F(cons(x, a), k)
F(a, empty) → G(a, empty)
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G(cons(x, k), d) → G(k, cons(x, d))
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(cons(x, k), d) → G(k, cons(x, d))
The value of delta used in the strict ordering is 9.
POL(cons(x1, x2)) = 3 + (4)x_1 + x_2
POL(G(x1, x2)) = (4)x_1 + x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
F(a, cons(x, k)) → F(cons(x, a), k)
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(a, cons(x, k)) → F(cons(x, a), k)
The value of delta used in the strict ordering is 1.
POL(cons(x1, x2)) = 1 + (3)x_1 + x_2
POL(F(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f(a, empty) → g(a, empty)
f(a, cons(x, k)) → f(cons(x, a), k)
g(empty, d) → d
g(cons(x, k), d) → g(k, cons(x, d))